@article{skalka,
  title={Classical Logic in a Judgemental Style},
  author={Christian Skalka},
  url={http://www.cs.uvm.edu/~ceskalka/303/nd.pdf}
}

@inproceedings{addingGenericity,
  title={Making the future safe for the past: Adding genericity to the Java programming language},
  author={Bracha, Gilad and Odersky, Martin and Stoutamire, David and Wadler, Philip},
  booktitle={ACM SIGPLAN Notices},
  volume={33},
  number={10},
  pages={183--200},
  year={1998},
  organization={ACM}
}

@article{GJ,
  title={GJ: Extending the JavaTM programming language with type parameters},
  author={Bracha, Gilad and Odersky, Martin and Stoutamire, David},
  journal={Sun Microsystems, University of South Australia, Bell Labs, Lucent Technologies},
  year={1998},
  publisher={Citeseer}
}

@inproceedings{addingWildcards,
  title={Adding wildcards to the Java programming language},
  author={Torgersen, Mads and Hansen, Christian Plesner and Ernst, Erik and von der Ah{\'e}, Peter and Bracha, Gilad and Gafter, Neal},
  booktitle={Proceedings of the 2004 ACM symposium on Applied computing},
  pages={1289--1296},
  year={2004},
  organization={ACM}
}

@incollection{ML,
  title={Proving ML type soundness within Coq},
  author={Dubois, Catherine},
  booktitle={Theorem Proving in Higher Order Logics},
  pages={126--144},
  year={2000},
  publisher={Springer}
}

@article{4color,
  title={Every planar map is four colorable. Part I: Discharging},
  author={Appel, Kenneth and Haken, Wolfgang},
  journal={Illinois Journal of Mathematics},
  volume={21},
  number={3},
  pages={429--490},
  year={1977},
  publisher={University of Illinois at Urbana-Champaign, Department of Mathematics}
}

@article{gonthier,
  title={A computer-checked proof of the four colour theorem},
  author={Gonthier, Georges},
  journal={preprint, Microsoft Research Cambridge},
  year={2005}
}

@incollection{exp,
  title={On the expressive power of programming languages},
  author={Felleisen, Matthias},
  booktitle={ESOP'90},
  pages={134--151},
  year={1990},
  publisher={Springer}
}

@online{popl,
  title={POPLmark Wiki},
  url={http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/}
}

@online{ccorn,
  title={Constructive Coq Repository at Nijmegen},
  url={http://corn.cs.ru.nl/}
}

@online{coqTactics,
  title={Tactics in the Coq reference manual},
  url={http://coq.inria.fr/refman/tactic-index.html}
}


@online{coqmath,
  title={Cocorico math project list},
  url={http://coq.inria.fr/cocorico/List%20of%20Coq%20Math%20Projects}
}

@online{cocorico,
  title={Cocorico Wiki},
  url={http://coq.inria.fr/cocorico/decompose%20records%20%28tactic%29}
}

@article{geuvers,
  title={Proof assistants: History, ideas and future},
  author={Geuvers, Herman},
  journal={Sadhana},
  volume={34},
  number={1},
  pages={3--25},
  year={2009},
  publisher={Springer}
}

@article{jFP,
  title={Lightweight Family Polymorphism},
  author={Igarashi, Atsushi and Saito, Chieri and Viroli, Mirko},
  url={http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/papers/pdf/lfp-JFP.pdf}
}

@article{wright,
 author = {Wright, Andrew K. and Felleisen, Matthias},
 title = {A syntactic approach to type soundness},
 journal = {Inf. Comput.},
 issue_date = {Nov. 15, 1994},
 volume = {115},
 number = {1},
 month = nov,
 year = {1994},
 issn = {0890-5401},
 pages = {38--94},
 numpages = {57},
 url = {http://dx.doi.org/10.1006/inco.1994.1093},
 doi = {10.1006/inco.1994.1093},
 acmid = {191909},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
} 

@book{pierce,
  title={Types and programming languages},
  author={Pierce, Benjamin C},
  journal={Types and programming languages},
  year=2002,
  publisher={The MIT Press}
}

@article{FJ,
  title={Featherweight Java: a minimal core calculus for Java and GJ},
  author={Igarashi, Atsushi and Pierce, Benjamin C and Wadler, Philip},
  journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume=23,
  number=3,
  pages={396--450},
  year=2001,
  publisher={ACM}
}

@article{dotFJ,
  title={Lightweight Family Polymorphism},
  author={Igarashi, Atsushi and Saito, Chieri and Viroli, Mirko},
  booktitle={Programming Languages and Systems},
  pages={161--177},
  year={2005},
  publisher={Springer}
}

@online{oracleGenerics,
  title={Oracle's Java documentation page},
  url={http://docs.oracle.com/javase/1.5.0/docs/guide/language/index.html}
}

@online{FJcode,
  title={FJ type safety proof code},
  author={Bruno De Fraine},
  url={http://soft.vub.ac.be/~bdefrain/featherj/}
}

@online{frontCoq,
  title={The Coq Proof Assistant},
  url={http://coq.inria.fr/}
}

@online{aboutCoq,
  title={The Coq Proof Assistant},
  url={http://coq.inria.fr/what-is-coq}
}

@article{milner,
  title={A theory of type polymorphism in programming},
  author={Milner, Robin},
  journal={Journal of computer and system sciences},
  volume=17,
  number=3,
  pages={348--375},
  year=1978,
  publisher={Elsevier}
}

@article{fampoly,
  title={Family polymorphism},
  author={Ernst, Erik},
  booktitle={ECOOP 2001 Object-Oriented Programming},
  pages={303--326},
  year={2001},
  publisher={Springer}
}
